T:Type, R:(TT).
(x, y:T. (R^+(x,y))  ((R^+(y,x))))
 (a, b, c:T. (R(a,b) & R(a,c))  (b = c))
 (x, y:T. (R(x,y))  (R^+!(x,y))) 

latex

Definitions	Type, t  T, , x:AB(x), R^+, f(a), x:A. B(x), A, P  Q, s = t, x:A  B(x), P & Q, R!, P  Q, P  Q, Void, False, x f y, A c B, x:A. B(x), R^*, s ~ t, {T}, SQType(T), left + right, P  Q, {x:A| B(x)} , , Dec(P), #$n, , a < b, (i = j), b, b, , rel_exp(T;R;n), A  B, , -n, n+m, n - m
Lemmas	le wf, rel exp wf, nat plus inc, bool cases, eqtt to assert, bool sq, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, assert wf, decidable int equal, nat plus properties, rel-star-iff-rel-plus-or, rel star wf, rel plus iff2, rel-rel-plus, rel-immediate wf, rel plus wf, not wf